

(* A prog is a list of decl and rules *)

type ('info, 'node) node = { data : 'info;
			     node : 'node }

and loc = Lexing.position * Lexing.position

and ident = (loc, string) node

type compop = Bne | Bge | Ble | Beq | Blt | Bgt
type logicop = Band | Bor
type unop = Uplus | Uminus | Udecr | Unotzero | Uiszero | Unot

type arithop = Bplus | Bminus
    
(* type 'info prog = int list *)

type 'info prog = 'info decl list * 'info proc list

and 'info proc = ident * 'info stmts
    
and 'info decl =
  | Dtype of typedecl
  | Dvar of vardecl

and typedecl = ident * ident list

and vardecl =
  | VDconst of ident * typ
  | VDglobal of ident * typ
  | VDarray of ident * typ * typ 

and typ =
  | Tany
  | Tlinenum of loc
  | Tproc
  | Tproccnt
  | Tbool
  | Treal
  | Tint
  | Tident of ident
      
and 'info stmts = 'info stmt list

and 'info stmt = ('info, 'info stmt_node) node
and 'info stmt_node =
  | Sawait of 'info qterm * 'info stmt option
  | Satomic of 'info stmts
  | Sassign of 'info leftval * 'info term
  | Sifelse of 'info qterm * 'info stmts * 'info stmts
  | Sassert of 'info qterm
  | Scritical
  | Swhile of 'info qterm * 'info stmts

and 'info atomic_term = ('info, 'info atomic_term_node) node
and 'info atomic_term_node =
  | ATleftval of 'info leftval
  | ATconstnum of 'info constnum
  | ATenum of ident
  | ATbool of bool


and 'info constnum = ('info, 'info constnum_node) node
and 'info constnum_node =
  | Creal of float
  | Cint of int32
      
and 'info leftval = ('info, 'info leftval_node) node
and 'info leftval_node =
  | LVident of ident
  | LVaccess of ident * ident list

      
and 'info term = ('info, 'info term_node) node
and 'info term_node =
  | TMatom of 'info atomic_term
  | TMarith of arithop * 'info atomic_term * 'info constnum


and 'info logic_term = ('info, 'info logic_term_node) node
and 'info logic_term_node =
  | LTterm of 'info term
  | LTlit of 'info literal
  | LTop of logicop * 'info logic_term * 'info logic_term


and 'info literal = ('info, 'info literal_node) node
and 'info literal_node = compop * 'info term * 'info term
      
and 'info qterm = ('info, 'info qterm_node) node
and 'info qterm_node =
  | Qterm of 'info logic_term
  | Qquantifier of quantifier * ident * 'info logic_term

and quantifier = Qexists | Qforall
      









